$\forall$$E$:Type. Tree($E$) $\subseteq$ tree\_con($E$;Tree($E$))